
#include <iostream>
#include "PDTEvalTraversal.h"
#include "PDTCodeGraph.h"

#include "PDTNumVar.h"
#include "PDTExpBoolBinNumDerived.h"
#include "PDTExpNumBinDerived.h"
#include "PDTProp.h"
#include "PDTNumConst.h"
#include "PDTAssign.h"
#include "PDTBoolVar.h"
#include "PDTExpBoolBinBoolDerived.h"
#include "PDTSetOp.h"
#include "PDTIfElse.h"
#include "PDTAssert.h"
#include "PDTListOfStatements.h"
#include "PDTType.h"
#include "PDTSetVar.h"
#include "PDTQuantifier.h"
#include "PDTBoolConst.h"
#include "PDTNeg.h"
#include "PDTNot.h"
#include "PDTWhile.h"
#include "PDTFunction.h"
#include "PDTBehavior.h"
#include "PDTMapConst.h"

#if 0
#define PDT_DEBUG_LINE  {olog () << d.getNodeString() << endl;}
#else
#define PDT_DEBUG_LINE
#endif

PDTEvalTraversal :: PDTEvalTraversal(PDTCodeGraph & aCG)
    : cg(aCG), size(cg.nodes.size())
{
    values = new PDTConst *[size];
    for (unsigned int i = 0; i < size; i++)
        values[i] = NULL;
}

PDTEvalTraversal :: ~PDTEvalTraversal() {
#if 0
    for (unsigned int i = 0; i < size; i++)
        delete values[i];
#endif
    delete [] values;
}

bool 
PDTEvalTraversal :: setValue(PDTNode & d, PDTConst * val) {
    unsigned int idx = d.getId();
    values[idx] = val;
    return true;
}

PDTConst * 
PDTEvalTraversal :: getChildValue(PDTNode & d, unsigned int i) const {
    vector<PDTNode * > & children = d.getChildren();
    PDTNode * child = children[i];
    PDTConst * val = getValue(*child);
    return val;
}

PDTConst * 
PDTEvalTraversal :: getValue(PDTNode & d) const {
    unsigned int id = d.getId();
    return values[id];
}

PDTConst * 
PDTEvalTraversal :: getValue(PDTNode * d) const {
    return getValue(*d);
}

typedef long long llint;


#define EVAL_BINARY_OP_LR(RESULT_T,OP,LEFT_T,RIGHT_T) \
    PDTConst * lft = getChildValue(d, 0); \
    if (lft == NULL) return Traversal::Stop; \
    PDTConst * rgt =  getChildValue(d, 1); \
    if (rgt == NULL) return Traversal::Stop; \
    LEFT_T ddd_l = (LEFT_T)0;RIGHT_T ddd_r = (RIGHT_T) 0; \
    LEFT_T l = lft->getConcrete(ddd_l); \
    RIGHT_T r = rgt->getConcrete(ddd_r); \
    RESULT_T result = l OP r; \
    PDTConst * value = PDTConst::makeConst(cg,result); \
    if (value == NULL) return Traversal::Stop; \
    setValue(d,value); \
    return  Traversal::Continue;

#define EVAL_BINARY_OP(TYPE,OP) \
        EVAL_BINARY_OP_LR(TYPE,OP,TYPE,TYPE)

#define EVAL_UNARY_OP(TYPE_T, OP) \
    PDTConst * cValue = getChildValue(d,0); \
    if (cValue == NULL) \
        return Traversal::Stop; \
    TYPE_T ddd = (TYPE_T) 0; \
    TYPE_T operand = cValue->getConcrete(ddd); \
    TYPE_T result = OP operand; \
    PDTConst * value = PDTConst::makeConst(cg, result); \
    if (value == NULL) \
        return Traversal::Stop; \
    setValue(d,value); \
    return Traversal::Continue;

#define EVAL_CONST() \
    if (getValue(d) == NULL) \
         setValue(d,&d); \
    return Traversal::Continue;

#define NOT_IMPLEMENTED_YET \
    olog() << "Not implemented yet!" << endl;


// PDTAdd 
Traversal::RetType PDTEvalTraversal :: post(PDTAdd & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP(llint,+)
}


// PDTAnd 
Traversal::RetType PDTEvalTraversal :: post(PDTAnd & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP(bool,&&)
}

// PDTAssert 
Traversal::RetType PDTEvalTraversal :: post(PDTAssert & d) {
  PDT_DEBUG_LINE

    PDTExpBool *  exp = d.getExpression();
    PDTConst * val = getValue(exp);
    setValue(d,val);
    return Traversal::Continue;
}

// PDTAssign 
Traversal::RetType PDTEvalTraversal :: beforeChild(PDTAssign & d, unsigned int i) {
  PDT_DEBUG_LINE

    if (i == 0) { // child 0 is the target 
        return Traversal::Skip;
    }
    return Traversal::Continue;
}


Traversal::RetType PDTEvalTraversal :: post(PDTAssign & d) {
  PDT_DEBUG_LINE

    PDTExp * exp = d.getExpression();
    PDTConst * v = getValue(exp);
    if (v == NULL)
        return Traversal::Stop;
    PDTVar * var = d.getTarget();
    PDTNode * varNode = var->getNode();
    if (varNode->isSequenceAccessNum() || varNode->isSequenceAccessBool()){
        PDTNode * idxExp = NULL;
        if (varNode->isSequenceAccessNum()) {
            idxExp = dynamic_cast<PDTSequenceAccessNum*>(var)->getRight();
        } else {
            idxExp = dynamic_cast<PDTSequenceAccessBool*>(var)->getRight();
        }
        if (idxExp->traverseEx(*this) == Traversal::Stop)
            return Traversal::Stop;
        PDTConst * idx = getValue(idxExp);
        if (idx == NULL)
            return Traversal::Stop;
        llint ddd = 0;
        llint i = idx->getConcrete(ddd);

        PDTSequence * seq = NULL;
        if (varNode->isSequenceAccessNum()) {
            idxExp = dynamic_cast<PDTSequenceAccessNum*>(var)->getLeft();
        } else {
            idxExp = dynamic_cast<PDTSequenceAccessBool*>(var)->getLeft();
        }
        PDTConst * seqValue = getValue(seq);
        if (seqValue == NULL) {
            seqValue = (PDTConst*)new PDTMapConst();
            setValue(*seq, seqValue);
        }
        PDTMapConst * seqMValue = dynamic_cast<PDTMapConst*>(seqValue);
        if (seqMValue == NULL) {
            pdt_throw PDTConstTypeEx;
        }
        seqMValue->setElement(i, v);
        return Traversal::Continue;
    }
    setValue(*var, v);
    if ( d.isReturnAssignStatement())
        throw PDTReturnStatementEx;// this is not a pdt_throw on purpose
                                   // should be caught to stop function
                                   // execution

    //TODO: set the value of the assign node itself to a tick!
    return Traversal::Continue;
}

// PDTBehavior 
Traversal::RetType PDTEvalTraversal :: pre(PDTBehavior & d){
  PDT_DEBUG_LINE

        return Traversal::Skip;
}

// PDTBehaviors 
Traversal::RetType PDTEvalTraversal :: pre(PDTBehaviors & d){
  PDT_DEBUG_LINE

    return Traversal::Skip;
}

#if 0
// PDTBehavior 
Traversal::RetType PDTEvalTraversal :: post(PDTBehavior & d) {
  PDT_DEBUG_LINE

    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTBehaviors 
Traversal::RetType PDTEvalTraversal :: post(PDTBehaviors & d) {
  PDT_DEBUG_LINE

    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}
#endif


// PDTBoolConst 
Traversal::RetType PDTEvalTraversal :: post(PDTBoolConst & d) {
  PDT_DEBUG_LINE

    EVAL_CONST()
    return Traversal::Continue;
}



// PDTBoolVar 
Traversal::RetType PDTEvalTraversal :: post(PDTBoolVar & d) {
  PDT_DEBUG_LINE

    if (getValue(d) == NULL) {
        bool b = (rand() % 2) ? true : false;
        PDTConst * v = PDTConst::makeConst(cg,b);
        setValue(d,v);
        elog() << "Variable " << d.getName() << " is used before being defined! Using a random value of "<< b << endl;
    }
    return Traversal::Continue;
}

// PDTConstSequence 
Traversal::RetType PDTEvalTraversal :: post(PDTConstSequence & d) {
  PDT_DEBUG_LINE

    PDTConst * val = getValue(d);
    if (val == NULL) {
        /* // if the size is zero then it maybe an empty string which is legal
        if (d.getSize() == 0) 
            return Traversal::Continue;
            */ 
        PDTMapConst * seqMValue = new PDTMapConst();
        for (unsigned int i = 0; i < d.getSize(); i++) {
            PDTNode * el = d.getElementAt(i);
            Traversal::RetType rc = el->traverseEx(*this);
            if (rc == Traversal::Stop){
                delete seqMValue;
                return Traversal::Stop;
            }
            PDTConst * v = getValue(el);
            seqMValue->setElement(i,v);
        }
        setValue(d,seqMValue);
    }
    return Traversal::Continue;
}

// PDTDiv 
Traversal::RetType PDTEvalTraversal :: post(PDTDiv & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP(llint,/)
}


// PDTEqualBool 
Traversal::RetType PDTEvalTraversal :: post(PDTEqualBool & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP(bool,==)
}


// PDTEqualNum 
Traversal::RetType PDTEvalTraversal :: post(PDTEqualNum & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP_LR(bool,==,llint,llint)
}



// PDTExist 

//the following is a recursive function to enumerate all
// values in the ranges of the quantifier variables
Traversal::RetType PDTEvalTraversal :: enumerateRanges (PDTQuantifier& d, unsigned int varIdx ) {
  PDT_DEBUG_LINE

    PDTExp * exp = d.getExpBool();
    if (varIdx == d.getNumVars()) {
        return exp->traverseEx(*this);
    }
    Traversal::RetType rc;
    PDTNode * var = d.getVarNode(varIdx); //the variables involved
    if (var->isNumVar()) {
        PDTNumVar* numVar = dynamic_cast<PDTNumVar*>(var);
        PDTIntRange * varRange = numVar->getRange();   
        long long start = 0;
        long long end = 4;
        if (varRange == NULL) {
            elog() << "Quantifier variable has no range, evaluating from 0 to 4." << endl;
        } else if (varRange->traverseEx(*this) == Traversal::Stop) {
            return Traversal::Stop;
        } else {
            PDTConst * startConst = getValue(varRange->getStart());
            PDTConst * endConst = getValue(varRange->getEnd());
            //TODO: add a message in case the value is not constant!
            start = startConst->getNumber();
            end = endConst->getNumber();
        }

        for (; start <= end; start++) {
            PDTConst * v = PDTConst::makeConst(cg,start);
            setValue(*var,v);
            rc = enumerateRanges(d, varIdx+1);
            if (rc != Traversal::Continue) 
                return rc;

            v = getValue(*exp);
            bool b = v->getBoolean();
            if ( (d.isExist() && b) || (d.isForall() && !b) ){
                setValue(d,v);
                return Traversal::Skip;
            }
        }
    } else if (var->isBoolVar()) {
        setValue(*var,PDTConst::makeConst(cg,true));
        rc = enumerateRanges(d, varIdx+1);
        if (rc != Traversal::Continue) 
            return rc;

        PDTConst * v = getValue(*exp);
        bool b = v->getBoolean();
        if ( (d.isExist() && b) || (d.isForall() && !b) ){
            setValue(d,v);
            return Traversal::Skip;
        }

        setValue(*var,PDTConst::makeConst(cg,false));
        rc = enumerateRanges(d, varIdx+1);
        if (rc != Traversal::Continue) 
            return rc;

        v = getValue(*exp);
        b = v->getBoolean();
        if ( (d.isExist() && b) || (d.isForall() && !b) ){
            setValue(d,v);
            return Traversal::Skip;
        }
    }
    PDTConst * v = PDTConst::makeConst(cg,d.isForall());
    setValue(d,v);
    return Traversal::Continue;
}

//IMPORTANT: 
// Exist and Forall use pre and return Skip because
// their evaluation sets the quantifier bound variables
// several times and evaluates the expression of the 
// body of the quantifier several times. 
// This can not be done simply with the default Traversal
// interface.
Traversal::RetType PDTEvalTraversal :: pre(PDTExist& d) {
  PDT_DEBUG_LINE

    Traversal::RetType rc = enumerateRanges(d, 0);
    if (rc == Traversal::Stop) 
        return Traversal::Stop;
    return Traversal::Skip;
}

// PDTForall 
Traversal::RetType PDTEvalTraversal :: pre(PDTForall & d) {
  PDT_DEBUG_LINE

    Traversal::RetType rc = enumerateRanges(d, 0);
    if (rc == Traversal::Stop) 
        return Traversal::Stop;
    return Traversal::Skip;
}

Traversal::RetType PDTEvalTraversal :: scasize(PDTFunctionCall & d) {
  PDT_DEBUG_LINE

    if (d.getArgumentCount() != 1) {
        cerr << "special function scasize has a wrong number of arguments. evaluation aborted!" << endl;
        return Traversal::Stop;
    }
    PDTNode * arg = d.getArgument(0);
    if (!arg->isSequenceVar()) {
        cerr << "special function scasize has a wrong type of argument. argument should be an array. evaluation aborted!" << endl;
        return Traversal::Stop;
    }
    PDTConst * argVal = getValue(arg);
    PDTMapConst * seqMValue = dynamic_cast<PDTMapConst*>(argVal);
    if (seqMValue == NULL) {
        pdt_throw PDTConstTypeEx;
    }
    llint size = seqMValue->getSize();
    PDTConst * value = PDTConst::makeConst(cg,size);
    setValue(d, value);
    return Traversal::Skip;
}

Traversal::RetType PDTEvalTraversal :: scchar(PDTFunctionCall & d, char ch) {
  PDT_DEBUG_LINE

    if (d.getArgumentCount() != 1) {
        cerr << "special function scasize has a wrong number of arguments. evaluation aborted!" << endl;
        return Traversal::Stop;
    }
    PDTNode * arg = d.getArgument(0);
    PDTConst * argVal = getValue(arg);
    char v = argVal->getNumber();
    bool result = (v == ch);
    PDTConst * value = PDTConst::makeConst(cg,result);
    setValue(d, value);
    return Traversal::Skip;
}

Traversal::RetType PDTEvalTraversal :: sccharrange(PDTFunctionCall & d, char ch1, char ch2) {
  PDT_DEBUG_LINE

    if (d.getArgumentCount() != 1) {
        cerr << "special function scasize has a wrong number of arguments. evaluation aborted!" << endl;
        return Traversal::Stop;
    }
    PDTNode * arg = d.getArgument(0);
    PDTConst * argVal = getValue(arg);
    char ch = argVal->getNumber();
    bool result = (ch1 <= ch && ch <= ch2);
    PDTConst * value = PDTConst::makeConst(cg,result);
    setValue(d, value);
    return Traversal::Skip;
}

Traversal::RetType PDTEvalTraversal :: scalphanum(PDTFunctionCall & d) {
  PDT_DEBUG_LINE

    if (d.getArgumentCount() != 1) {
        cerr << "special function scasize has a wrong number of arguments. evaluation aborted!" << endl;
        return Traversal::Stop;
    }
    PDTNode * arg = d.getArgument(0);
    PDTConst * argVal = getValue(arg);
    char ch = argVal->getNumber();
    bool result = (ch <= 'a' && ch <= 'z') ||
        (ch <= '0' && ch <= '9');
    PDTConst * value = PDTConst::makeConst(cg,result);
    setValue(d, value);
    return Traversal::Skip;
}

// PDTFunctionCall 
Traversal::RetType PDTEvalTraversal :: post(PDTFunctionCall & d) {
  PDT_DEBUG_LINE

    PDTFunctionDec * funcDec = d.getFuncPtr();
    if (d.isSpecial() || 
        funcDec == NULL || 
        (PDTNode*)funcDec == (PDTNode*)&PDTUnresolvedExp::unresolvedExp) {
        string name = d.getName();
        if (name == "scasize")  {
            return scasize(d);
        } else if (name == "scblank"){
            return scchar(d,' ');
        } else if (name == "scnewline") {
            return scchar(d,'N');
        } else if (name == "scalpha") {
            return sccharrange(d,'a','z');
        } else if (name == "scnum") {
            return sccharrange(d,'0','9');
        } else if (name == "scalphanum") {
            return scalphanum(d);
        } 
        olog() << "a special function " << d.getName() << " does not have an internal implementation. internal error." << endl;
        return Traversal::Stop;
    }

    vector<PDTVar * > vars;
    for (unsigned int i = 0; i < cg.variables.size(); i++) {
        if (cg.variables[i]->getFunctionDec() == funcDec) {
            vars.push_back(cg.variables[i]);
        }
    }
    // save old values: needed for recursive calls.
    PDTConst ** oldVals = new PDTConst*[vars.size()];
    for (unsigned int i = 0; i < vars.size(); i++) {
        oldVals[i] = getValue(*vars[i]);
    }

    assert(d.getArgumentCount() == funcDec->getArgumentCount());

    // copy the values from the argument list to the argument vars
    for (unsigned int i = 0; i < d.getArgumentCount(); i++) {
        PDTNode * arg = d.getArgument(i);
        PDTConst * argVal = getValue(arg);
        PDTVar * argVar = funcDec->getArgument(i);
        cout << "setting value of  argument " << argVar->getName() << " to ";
        if (argVal != NULL) {
            stringstream ss;
            argVal->getNode()->toString(ss);
            cout << ss.str();
        } else {
            cout << "NULL";
        }
        cout << endl;
        PDTNode * argVarNode = argVar->getNode();
        setValue(*argVarNode, argVal);
    }
    Traversal::RetType rc = Traversal::Continue;
    try{
        rc = funcDec->traverseEx(*this);
    } catch (PDTCheckSpecException e) {
        if (e == PDTReturnStatementEx) {
            rc = Traversal::Continue;
        } else  {
            pdt_throw e;
        }
    } catch (...) {
        cout << "caugth an exception." << endl;
    }

    if (rc == Traversal::Stop) {
        delete [] oldVals;
        return Traversal::Stop;
    }

    PDTVar * retVar = funcDec->getReturnVar();
    PDTNode * retVarNode = retVar->getNode();
    PDTConst * val = getValue(retVarNode);
    setValue(d,val);

    //reset the old values: needed for recursive calls!
    //IMPORTANT: watch for the return variable!
    for (unsigned int i = 0; i < vars.size(); i++) {
        setValue(*vars[i], oldVals[i]);
    }
    delete [] oldVals;

    return Traversal::Continue;
}
#if 0
// PDTFunctionDec 
Traversal::RetType PDTEvalTraversal :: post(PDTFunctionDec & d) {
  PDT_DEBUG_LINE

    if (getValue(d) != NULL)
        return Traversal::Continue;

    unsigned int i = 0; 
    vector <PDTVar *> args; 
    for (; i < d.argc; i++) {
        PDTNode * clone = getChildValue(d,i); 
        PDTVar * vValue = dynamic_cast<PDTVar *>(clone);
        if (vValue == NULL)
            return Traversal::Stop;
        args.push_back(vValue);
    } 
    PDTVar * retVar  = d.getReturnVar();
    PDTNode * retNode = retVar->getNode();
    PDTNode * retValue = getValue(*retNode);
    PDTVar * retVarValue = dynamic_cast<PDTVar*>(retValue);
    if (retVarValue == NULL)
        return Traversal::Stop;

    PDTListOfStatements* list = d.getStatements();
    PDTNode * listNodeValue = getValue(*bodyValue);
    PDTListOfStatements* listValue = dynamic_cast<PDTListOfStatements*>(listNodeValue);
    if (listValue == NULL) 
        return Traversal::Stop;

    string & name = d.getName();

    PDTFunctionDec * clone = new PDTFunctionDec(cg, name,*listCLone, retVarValue, args);

    if (clone == NULL)
        return Traversal::Stop;
    setValue(d,clone);
    return Traversal::Continue;
}
#endif

// PDTGreaterThan 
Traversal::RetType PDTEvalTraversal :: post(PDTGreaterThan & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP_LR(bool,>,llint,llint)
}


// PDTGreaterThanEqual 
Traversal::RetType PDTEvalTraversal :: post(PDTGreaterThanEqual & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP_LR(bool,>=,llint,llint)
}

// PDTIfElse 
Traversal::RetType PDTEvalTraversal :: beforeChild(PDTIfElse & d, unsigned int i) {
  PDT_DEBUG_LINE

    if (i == PDTIfElse::IfIdx) {
        PDTConst * condVal = getValue(d.getCondition());
        bool b = condVal->getBoolean();
        if (!b)
            return Traversal::Skip;
    } else if (i == PDTIfElse::ElseIdx) {
        PDTConst * condVal = getValue(d.getCondition());
        bool b = condVal->getBoolean();
        if (b)
            return Traversal::Skip;
    }
    return Traversal::Continue;
}

Traversal::RetType PDTEvalTraversal :: post(PDTIfElse & d) {
  PDT_DEBUG_LINE

    return Traversal::Continue;
}

// PDTImplies 
Traversal::RetType PDTEvalTraversal :: beforeChild(PDTImplies& d, unsigned int i) {
  PDT_DEBUG_LINE

    if (i == 1) {// the right hand side child
        PDTConst * lft = getChildValue(d, 0); 
        if (lft == NULL) 
            return Traversal::Stop;
        bool ddd=false;
        bool l = lft->getConcrete(ddd);
        if (l == false)
            return  Traversal::Skip;
    }
    return  Traversal::Continue;
}

Traversal::RetType PDTEvalTraversal :: post(PDTImplies & d) {
  PDT_DEBUG_LINE

    PDTConst * lft = getChildValue(d, 0); 
    if (lft == NULL) 
        return Traversal::Stop;
    bool ddd=false;
    bool l = lft->getConcrete(ddd);
    bool result = true;
    if (l == false) {
        result = true;
    } else {
        PDTConst * rgt =  getChildValue(d, 1);
        if (rgt == NULL) 
            return Traversal::Stop;
        bool r = rgt->getConcrete(ddd);
        result = (!l) || r;
    }
    PDTConst * value = PDTConst::makeConst(cg,result); 
    if (value == NULL) 
        return Traversal::Stop;
    setValue(d,value);
    return  Traversal::Continue;
}



// PDTIntRange 
Traversal::RetType PDTEvalTraversal :: post(PDTIntRange & d) {
  PDT_DEBUG_LINE

    return Traversal::Continue;
}

// PDTInvariant 
Traversal::RetType PDTEvalTraversal :: post(PDTInvariant & d) {
  PDT_DEBUG_LINE

    PDTExpBool *  exp = d.getExpression();
    PDTConst * val = getValue(exp);
    setValue(d,val);
    return Traversal::Continue;
}

// PDTLessThan 
Traversal::RetType PDTEvalTraversal :: post(PDTLessThan & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP_LR(bool,<,llint,llint)
}


// PDTLessThanEqual 
Traversal::RetType PDTEvalTraversal :: post(PDTLessThanEqual & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP_LR(bool,<=,llint,llint)
}
#if 0

// PDTListOfStatements 
Traversal::RetType PDTEvalTraversal :: post(PDTListOfStatements & d) {
  PDT_DEBUG_LINE

    vector<PDTStatement*> statements;
    for (unsigned int i=0; i<d.numberOfStmts(); i++){
        PDTNode * clone = getChildValue(d,i);
        PDTStatement * statement = dynamic_cast<PDTStatement*>(clone);
        if (statement == NULL)
            return Traversal::Stop;
        statements.push_back(statement);
    }
    PDTListOfStatements * clone = new PDTListOfStatements(cv, statements);
    if (clone == NULL)
        return Traversal::Stop;
    setValue(d,clone);
    return Traversal::Continue;
}
#endif

// PDTMod 
Traversal::RetType PDTEvalTraversal :: post(PDTMod & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP(llint,%)
}


// PDTMult 
Traversal::RetType PDTEvalTraversal :: post(PDTMult & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP(llint,*)
}


// PDTNeg 
Traversal::RetType PDTEvalTraversal :: post(PDTNeg & d) {
  PDT_DEBUG_LINE

    EVAL_UNARY_OP(llint,-)
}

#if 0

// PDTNilStatement 
Traversal::RetType PDTEvalTraversal :: post(PDTNilStatement & d) {
  PDT_DEBUG_LINE

    if(getValue(d) == NULL)
        setValue(d,&d);
    return Traversal::Continue;
}
#endif


// PDTNot 
Traversal::RetType PDTEvalTraversal :: post(PDTNot & d) {
  PDT_DEBUG_LINE

   EVAL_UNARY_OP(bool, !) 
}


// PDTNotEqualBool 
Traversal::RetType PDTEvalTraversal :: post(PDTNotEqualBool & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP(bool,!=)
}


// PDTNotEqualNum 
Traversal::RetType PDTEvalTraversal :: post(PDTNotEqualNum & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP_LR(bool,!=,llint,llint)
}



// PDTNumConst 
Traversal::RetType PDTEvalTraversal :: post(PDTNumConst & d) {
  PDT_DEBUG_LINE

    EVAL_CONST()
}


// PDTNumConstDbl 
Traversal::RetType PDTEvalTraversal :: post(PDTNumConstDbl & d) {
  PDT_DEBUG_LINE

    EVAL_CONST()
}


// PDTNumConstInt 
Traversal::RetType PDTEvalTraversal :: post(PDTNumConstInt & d) {
  PDT_DEBUG_LINE

    EVAL_CONST()
}


// PDTNumVar 
Traversal::RetType PDTEvalTraversal :: post(PDTNumVar & d) {
  PDT_DEBUG_LINE

    if (getValue(d) == NULL) {
        llint v = rand();
        PDTConst * vConst = PDTConst::makeConst(cg,v);
        setValue(d,vConst);
        elog() << "Variable " << d.getName() << " is used before being defined! Using a random value: "<< v << "." <<  endl;
    }
    return Traversal::Continue;
}


// PDTOr 
Traversal::RetType PDTEvalTraversal :: post(PDTOr & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP(bool,||)
}


// PDTPair 
Traversal::RetType PDTEvalTraversal :: post(PDTPair & d) {
  PDT_DEBUG_LINE

    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}

// PDTPostCondition 
Traversal::RetType PDTEvalTraversal :: post(PDTPostCondition & d) {
  PDT_DEBUG_LINE

    PDTExpBool *  exp = d.getExpression();
    PDTConst * val = getValue(exp);
    setValue(d,val);
    return Traversal::Continue;
}


// PDTPreCondition 
Traversal::RetType PDTEvalTraversal :: post(PDTPreCondition & d) {
  PDT_DEBUG_LINE

    PDTExpBool *  exp = d.getExpression();
    PDTConst * val = getValue(exp);
    setValue(d,val);
    return Traversal::Continue;
}


// PDTProp 
Traversal::RetType PDTEvalTraversal :: post(PDTProp & d) {
  PDT_DEBUG_LINE

    PDTExpBool *  exp = d.getOperand();
    PDTConst * val = getValue(exp);
    setValue(d,val);
    return Traversal::Continue;
}



// PDTRelation 
Traversal::RetType PDTEvalTraversal :: post(PDTRelation & d) {
  PDT_DEBUG_LINE

    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTSequence 
Traversal::RetType PDTEvalTraversal :: post(PDTSequence & d) {
  PDT_DEBUG_LINE

    PDTConst * valueSeq = getValue(d);
    if (valueSeq == NULL) {
        elog() << "Sequence with ID " << d.getId() << " is used before being defined. No values are assumed, please fix." << endl;
    }
    return Traversal::Continue;
}


// PDTSequenceAccessBool 
Traversal::RetType PDTEvalTraversal :: post(PDTSequenceAccessBool & d) {
  PDT_DEBUG_LINE

    PDTNode * idxExp = d.getRight();
    PDTConst * idx = getValue(idxExp);
    if (idx == NULL)
        return Traversal::Stop;

    llint ddd = 0;
    llint i = idx->getConcrete(ddd);

    PDTSequence * seq = d.getLeft();
    PDTConst * seqValue = getValue(seq);
    if (seqValue == NULL) {
        elog() << "Sequence " << d.getName() << " is used before being defined." << endl;
        seqValue = (PDTConst*)new PDTMapConst();
        setValue(*seq, seqValue);
    }
    PDTMapConst * seqMValue = dynamic_cast<PDTMapConst*>(seqValue);
    if (seqMValue == NULL) {
        pdt_throw PDTConstTypeEx;
    }

    PDTConst * el = seqMValue->getElement(i);
    if (el == NULL) {
        bool v = (rand()%2) ? true: false;
        el = PDTConst::makeConst(cg,v);
        seqMValue->setElement(i,el);
        elog() << "Element " << d.getName() << "[" << i << "] is used before being defined. Set using `rand()%2` to be " << v << "." << endl;
    }
    setValue(d,el);
    return Traversal::Continue;
}


// PDTSequenceAccessNum 
Traversal::RetType PDTEvalTraversal :: post(PDTSequenceAccessNum & d) {
  PDT_DEBUG_LINE

    PDTNode * idxExp = d.getRight();
    PDTConst * idx = getValue(idxExp);
    if (idx == NULL)
        return Traversal::Stop;

    llint ddd = 0;
    llint i = idx->getConcrete(ddd);

    PDTSequence * seq = d.getLeft();
    PDTConst * seqValue = getValue(seq);
    if (seqValue == NULL) {
        elog() << "Sequence " << d.getName() << " is used before being defined." << endl;
        seqValue = new PDTMapConst();
        setValue(*seq, seqValue);
    }
    PDTMapConst * seqMValue = dynamic_cast<PDTMapConst*>(seqValue);
    if (seqMValue == NULL) {
        pdt_throw PDTConstTypeEx;
    }

    PDTConst * el = seqMValue->getElement(i);
    if (el == NULL) {
        llint v = (rand()%2) ? true: false;
        el = PDTConst::makeConst(cg,v);
        seqMValue->setElement(i,el);
        elog() << "Element " << d.getName() << "[" << i << "] is used before being defined. Set using `rand()` to be " << v << "." << endl;
    }
    setValue(d,el);
    return Traversal::Continue;
}


// PDTSequenceAssign 
Traversal::RetType PDTEvalTraversal :: beforeChild(PDTSequenceAssign & d, unsigned int i) {
  PDT_DEBUG_LINE

    if (i == 0) {//target var
        return Traversal::Skip;
    }
    return Traversal::Continue;
}

Traversal::RetType PDTEvalTraversal :: post(PDTSequenceAssign & d) {
  PDT_DEBUG_LINE

    PDTVar * var = d.getTarget();
    PDTNode * varNode = var->getNode();

    PDTSequenceVar * seqVar = dynamic_cast<PDTSequenceVar*>(var);
    PDTSequence * seq = seqVar->getSequence();

    PDTConstSequence * rhsSeq = d.getSequenceConst();
    PDTConst * val = getValue(rhsSeq);

    //TODO: maybe free the value already on varNode and seq!
    setValue(*varNode, val);
    setValue(*seq, val);
    return Traversal::Continue;
}


// PDTSequenceVar 
Traversal::RetType PDTEvalTraversal :: post(PDTSequenceVar & d) {
  PDT_DEBUG_LINE

    PDTSequence * seq = d.getSequence();
    PDTConst * valueSeq = getValue(seq);
    if (valueSeq == NULL) {
        elog() << "Sequence var " << d.getName() << " is used before being defined. No values are assumed, please fix." << endl;
    }
    return Traversal::Continue;
}

#if 0

// PDTSet 
Traversal::RetType PDTEvalTraversal :: post(PDTSet & d) {
  PDT_DEBUG_LINE

    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTSetVar 
Traversal::RetType PDTEvalTraversal :: post(PDTSetVar & d) {
  PDT_DEBUG_LINE

    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}
#endif


// PDTSubt 
Traversal::RetType PDTEvalTraversal :: post(PDTSubt & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP(llint,-)
}


// PDTWhile 
Traversal::RetType PDTEvalTraversal :: pre(PDTWhile & d) {
  PDT_DEBUG_LINE

    PDTExpBool* cond = d.getCondition();
    PDTStatement* loop = d.getLoopStatement();
    while(true) {
        Traversal::RetType rc = cond->traverseEx(*this);
        if (rc == Traversal::Stop)
            return Traversal::Stop;
        PDTConst * condValue = getValue(cond);
        bool b = condValue->getBoolean();
        if (!b) 
            return Traversal::Continue;
        rc = loop->traverseEx(*this);
        if (rc == Traversal::Stop)
            return Traversal::Stop;
    }
    //TODO: check what is a good value to set!
    return Traversal::Skip;
}

// PDTXor 
Traversal::RetType PDTEvalTraversal :: post(PDTXor & d) {
  PDT_DEBUG_LINE

    EVAL_BINARY_OP(bool,!=)
}

// PDTUnresolvedExp 
Traversal::RetType PDTEvalTraversal :: post(PDTUnresolvedExp & d) {
  PDT_DEBUG_LINE

    pdt_throw PDTNotResolvedEx;
    return Traversal::Stop;
}

#if 0
// PDTType 
Traversal::RetType PDTEvalTraversal :: post(PDTType & d) {
  PDT_DEBUG_LINE

    CLONE_CONST()
}
#endif


// PDTUnaryNumExpr 
Traversal::RetType PDTEvalTraversal :: post(PDTUnaryNumExpr & d) {
  PDT_DEBUG_LINE

    EVAL_UNARY_OP(llint,-) 
}
